; benchmark generated from python API
(set-info :status unknown)
(declare-fun bottom_feasible () Bool)
(declare-fun bottom_kid_0_feasible () Bool)
(declare-fun bottom_kid_0_width () Real)
(declare-fun bottom_hight () Real)
(declare-fun bottom_kid_0_y () Real)
(declare-fun bottom_kid_0_hight () Real)
(declare-fun bottom_width () Real)
(declare-fun bottom_kid_0_x () Real)
(assert
 (let (($x5632 (= bottom_kid_0_width 100.0)))
 (let (($x5631 (= (- (+ bottom_kid_0_hight bottom_kid_0_y) bottom_hight) (- 10.0))))
 (let (($x5628 (= bottom_kid_0_y 10.0)))
 (let (($x5627 (>= (+ (- (- bottom_kid_0_hight) bottom_kid_0_y) bottom_hight) 10.0)))
 (let (($x5623 (>= bottom_kid_0_y 10.0)))
 (let (($x5622 (>= (- (+ (- bottom_kid_0_x) bottom_width) bottom_kid_0_width) 10.0)))
 (let (($x5618 (>= bottom_kid_0_x 10.0)))
 (let (($x5617 (= (+ (- (* 2.0 bottom_kid_0_x) bottom_width) bottom_kid_0_width) 0.0)))
 (let (($x5613 (>= bottom_kid_0_hight 0.0)))
 (let (($x5612 (>= bottom_kid_0_width 0.0)))
 (let (($x5611 (>= bottom_kid_0_y 0.0)))
 (let (($x5610 (>= bottom_kid_0_x 0.0)))
 (and $x5610 $x5611 $x5612 $x5613 $x5617 $x5618 $x5622 $x5623 $x5627 $x5628 $x5631 $x5632 bottom_kid_0_feasible bottom_feasible))))))))))))))
(check-sat)

